COMMENT ⊗   VALID 00009 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.REQUIRE "LSPMAC.PUB[LSP,CLT]" source_file
C00003 00003	.hd206 FALL 1979
C00006 00004	
C00007 00005	.bb Proving
C00009 00006	.bb Formal systems
C00010 00007	.bb Compiling
C00012 00008	.bb Games
C00013 00009	.bb Some previous projects.
C00014 ENDMK
C⊗;
.REQUIRE "LSPMAC.PUB[LSP,CLT]" source_file;
.
.MACRO  hd206 (TERM) ⊂
.BEGIN    NOFILL  TURNON "←→"
.place heading
←COMPUTER SCIENCE DEPARTMENT
←STANFORD UNIVERSITY
.place text
CS206  ←RECURSIVE PROGRAMMING AND PROVING →TERM
.TURNOFF
.END ⊃
.LSPFONT
.basicops 
.itemmac 1;
.
.PORTION MAINPORTION
.hd206 FALL 1979
.PAGE ← 1
.cb TERM PROJECTS

	A term project is not required in order to pass CS206 or even to
get a grade of B if your homework and exams are good enough.  However, if
you wish to get some flavor of A then doing a good term project is necessary.
Term projects will be due on the day of the final exam.  Any term project
turned in ahead of time will be likely to get a more thorough reading.

	The term project is your opportunity to direct your attention
to and get experience in some area that interests you.   Briefly
the possibilities include writing and documenting an substantial
LISP program, proving the correctness of a moderate sized LISP program,
or developing techniques and principles for proving properties
for some class of programs.

	The write up of your project is the main thing that will get
graded so it should be clear and carefully done.  It should include
a brief description of what you set out to do and what you accomplished.
If you write a progam, you should give a description of how it works
and why, including a description of the data structures it is acting
on and the basic operations on these structures.  The code
for the program should be included with brief comments in appropriate
places to guide the reader.  Some sample runs should also be included.

	The following are some ideas for term projects.  You may choose
one of these, or design your own project.
.bb Proving

#. Develop and apply techniques for proving properties of programs
manipulating graphs.  The proofs should be fully formal, but also
natual and cleanly expressible.

#.  Develop the theory of re-entrant list structures.  (see Chapter IV.)
Decide on a representation
of such structures as ordinary lists (say with pointers and labels).  Define
some primitive operations (for example: ⊗⊗car cdr cons point cut⊗).  Write programs
to go from one representation to the other.  Write an equality predicate in
for structures in your representation.   Work out an induction schema to
allow you to tell when programs on such structures will terminate.
Write some interesting programs on such structures and prove some facts
about them.

.bb Formal systems

#. Write a proof checker for a simple formal system.   Some examples
of suitable formal systems are:
.skip
.begin preface 0 indent 8,8

##. Trigonometric expressions: using trig identities to prove expressions
equivalent.

##. Symbolic integration: using various standard tricks for manipulating
integrands into integrable form.

##. Propositional logic and a Hilbert or natural deduction style proof
system.

Implement some heuristics to search for proofs.

Derived rules + ability to unwind.
.end

.bb Compiling
.begin indent 0,4

#. Improve the LCOM4 compiler.  Some possibilities are to modify LCOM4 to:
.begin nofill indent 8,8

##. compile  ⊗label. 
##. handle the %3prog%1 and related features.
##. handle functions as arguments (as for ⊗mapcar) .
##. recognize iteration and compile it with loops.
##. produce more efficient arithmetic code.
##. compile additional features such as "while's" or "do's" etc..
.end

#. Write a data driven compiler for LISP.

#. Write a syntax directed compiler for LISP.   Perhaps several passes using
an intermediate language would be useful.  

.bb Games

#. Write a program to play a game.  Some possible games are:
.begin nofill indent 8,8

##. 3-dimensional Tic Tac Toe (See Chapter II for 2-D version)
##. Solitare
##. Mastermind
##. Otello
.end

    There are two key issues in programs to play games.  One is
the method used to prune the search for possible moves, the other
is developing good strategies of choosing moves.  These issues are
of course not independent from one another.

    Be sure to hold individual test runs to a few seconds.  It is easy to
use large amounts of computer time in such projects.  

.bb Some previous projects.

#. Minimizing finite state machine

#. Digital Circuit design

#. LALR parser

.end